$\forall$$A$, $B$:Type, $P$:($A$$\rightarrow\mathbb{P}$), $d$:($x$:$A$$\rightarrow$Dec($P$($x$))), $f$:(\{$x$:$A$$\mid$ $P$($x$)\} $\rightarrow$$B$), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply(p{-}lift($d$;$f$);$x$)) $\Leftarrow\!\Rightarrow$ $P$($x$)